Logiweb aspects of system zf in pyk

Up Help

The predefined "pyk" aspect

define pyk of system zf as text unicode start of text unicode small s unicode small y unicode small s unicode small t unicode small e unicode small m unicode space unicode small z unicode small f unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of system zf as text unicode start of text unicode capital z unicode capital f unicode small s unicode small u unicode small b unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of system zf as all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var x end metavar zermelo is metavar var y end metavar imply for all objects object var var s end var indeed not0 object var var s end var zermelo in metavar var x end metavar imply object var var s end var zermelo in metavar var y end metavar imply not0 object var var s end var zermelo in metavar var y end metavar imply object var var s end var zermelo in metavar var x end metavar imply not0 for all objects object var var s end var indeed not0 object var var s end var zermelo in metavar var x end metavar imply object var var s end var zermelo in metavar var y end metavar imply not0 object var var s end var zermelo in metavar var y end metavar imply object var var s end var zermelo in metavar var x end metavar imply metavar var x end metavar zermelo is metavar var y end metavar rule plus all metavar var s end metavar indeed all metavar var x end metavar indeed not0 metavar var s end metavar zermelo in power metavar var x end metavar end power imply for all objects object var var s end var indeed object var var s end var zermelo in metavar var s end metavar imply object var var s end var zermelo in metavar var x end metavar imply not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var s end metavar imply object var var s end var zermelo in metavar var x end metavar imply metavar var s end metavar zermelo in power metavar var x end metavar end power rule plus all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar rule plus all metavar var r end metavar indeed all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var big set end metavar indeed not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar infer metavar var x end metavar zermelo in the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set infer metavar var y end metavar zermelo in the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set infer not0 metavar var x end metavar zermelo is metavar var y end metavar infer the set of ph in union zermelo pair zermelo pair metavar var x end metavar comma metavar var x end metavar end pair comma zermelo pair metavar var y end metavar comma metavar var y end metavar end pair end pair end union such that not0 placeholder-var var c end var zermelo in metavar var x end metavar imply not0 placeholder-var var c end var zermelo in metavar var y end metavar end set zermelo is zermelo empty set rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot 1deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end 1deduction endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var s end metavar zermelo in zermelo pair metavar var x end metavar comma metavar var y end metavar end pair imply not0 metavar var s end metavar zermelo is metavar var x end metavar imply metavar var s end metavar zermelo is metavar var y end metavar imply not0 not0 metavar var s end metavar zermelo is metavar var x end metavar imply metavar var s end metavar zermelo is metavar var y end metavar imply metavar var s end metavar zermelo in zermelo pair metavar var x end metavar comma metavar var y end metavar end pair rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar rule plus all metavar var x end metavar indeed all metavar var t end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed exist-sub0 quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var t end metavar end quote end sub endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var s end metavar indeed all metavar var x end metavar indeed not0 metavar var s end metavar zermelo in union metavar var x end metavar end union imply not0 metavar var s end metavar zermelo in existential var var j end var imply not0 existential var var j end var zermelo in metavar var x end metavar imply not0 not0 metavar var s end metavar zermelo in existential var var j end var imply not0 existential var var j end var zermelo in metavar var x end metavar imply metavar var s end metavar zermelo in union metavar var x end metavar end union rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer for all objects metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var p end metavar indeed all metavar var x end metavar indeed all metavar var z end metavar indeed metavar var p end metavar is placeholder-var and ph-sub0 quote metavar var b end metavar end quote is quote metavar var a end metavar end quote where quote metavar var p end metavar end quote is quote metavar var z end metavar end quote end sub endorse not0 metavar var z end metavar zermelo in the set of ph in metavar var x end metavar such that metavar var a end metavar end set imply not0 metavar var z end metavar zermelo in metavar var x end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var z end metavar zermelo in metavar var x end metavar imply not0 metavar var b end metavar imply metavar var z end metavar zermelo in the set of ph in metavar var x end metavar such that metavar var a end metavar end set rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var b end metavar imply metavar var a end metavar infer not0 metavar var b end metavar imply not0 metavar var a end metavar infer metavar var b end metavar rule plus all metavar var s end metavar indeed not0 metavar var s end metavar zermelo in zermelo empty set end define