begin
theorem
theorem
theorem
scheme
Fraenkel6A{
F1()
-> LATTICE,
F2(
set )
-> set ,
P1[
set ],
P2[
set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F2(v2) where v2 is Element of F1() : P2[v2] }
provided
A1:
for
v being
Element of
F1() holds
(
P1[
v] iff
P2[
v] )
theorem Th4:
theorem
theorem Th6:
begin
:: deftheorem defines Proj WAYBEL24:def 1 :
theorem Th7:
:: deftheorem defines Proj WAYBEL24:def 2 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
begin
:: deftheorem Def3 defines ContMaps WAYBEL24:def 3 :
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
Lm1:
for S being non empty RelStr
for D being non empty Subset of S holds D = { i where i is Element of S : i in D }
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem
theorem