consider R being Relation of F1() such that
A5: for x, y being Element of F1() holds
( [x,y] in R iff P1[x,y] ) from RELSET_1:sch 2();
 A6: R is_transitive_in F1()
proof
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A7: x in F1() and
A8: y in F1() and
A9: z in F1() ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider x9 = x, y9 = y, z9 = z as Element of F1() by A7, A8, A9;
assume that
A10: [x,y] in R and
A11: [y,z] in R ; :: thesis: [x,z] in R
A12: P1[y9,z9] by A5, A11;
P1[x9,y9] by A5, A10;
then P1[x9,z9] by A3, A12;
hence [x,z] in R by A5; :: thesis: verum
end;
F1() c= dom R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1() or x in dom R )
assume x in F1() ; :: thesis: x in dom R
then reconsider x9 = x as Element of F1() ;
P1[x9,x9] by A1;
then [x,x] in R by A5;
hence x in dom R by XTUPLE_0:def 12; :: thesis: verum
end;
then dom R = F1() ;
then A13: F1() c= field R by XBOOLE_1:7;
field R = (dom R) \/ (rng R) ;
then A14: field R = F1() by A13;
A15: R is_reflexive_in F1() by A1, A5;
A16: F1() has_lower_Zorn_property_wrt R
proof
let Y be set ; :: according to ORDERS_1:def 11 :: thesis: ( Y c= F1() & R |_2 Y is being_linear-order implies ex x being set st
( x in F1() & ( for y being set st y in Y holds
[x,y] in R ) ) )
assume that
A17: Y c= F1() and
A18: R |_2 Y is being_linear-order ; :: thesis: ex x being set st
( x in F1() & ( for y being set st y in Y holds
[x,y] in R ) )
for x, y being Element of F1() st x in Y & y in Y & P1[x,y] holds
P1[y,x]
proof
let x, y be Element of F1(); :: thesis: ( x in Y & y in Y & P1[x,y] implies P1[y,x] )
assume that
A19: x in Y and
A20: y in Y ; :: thesis: ( P1[x,y] or P1[y,x] )
A21: ( R |_2 Y is reflexive & R |_2 Y is connected ) by A18;
Y c= field (R |_2 Y)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in field (R |_2 Y) )
assume A22: x in Y ; :: thesis: x in field (R |_2 Y)
then A23: [x,x] in [:Y,Y:] by ZFMISC_1:87;
[x,x] in R by A15, A17, A22;
then [x,x] in R |_2 Y by A23, XBOOLE_0:def 4;
hence x in field (R |_2 Y) by RELAT_1:15; :: thesis: verum
end;
then A24: Y = field ((R |_2 Y) |_2 Y) by A21, Lm7
.= field (R |_2 Y) by WELLORD1:21 ;
then A25: R |_2 Y is_connected_in Y by A21;
A26: R |_2 Y is_reflexive_in Y by A21, A24;
( x = y or x <> y ) ;
then ( [x,y] in R |_2 Y or [y,x] in R |_2 Y ) by A19, A20, A25, A26;
then ( [x,y] in R or [y,x] in R ) by XBOOLE_0:def 4;
hence ( P1[x,y] or P1[y,x] ) by A5; :: thesis: verum
end;
then consider y being Element of F1() such that
A27: for x being Element of F1() st x in Y holds
P1[y,x] by A4, A17;
take y ; :: thesis: ( y in F1() & ( for y being set st y in Y holds
[y,y] in R ) )
thus y in F1() ; :: thesis: for y being set st y in Y holds
[y,y] in R
let x be set ; :: thesis: ( x in Y implies [y,x] in R )
assume A28: x in Y ; :: thesis: [y,x] in R
then P1[y,x] by A17, A27;
hence [y,x] in R by A5, A17, A28; :: thesis: verum
end;
R is_antisymmetric_in F1()
proof
let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in F1() or not y in F1() or not [x,y] in R or not [y,x] in R or x = y )
assume that
A29: x in F1() and
A30: y in F1() ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
reconsider x9 = x, y9 = y as Element of F1() by A29, A30;
assume that
A31: [x,y] in R and
A32: [y,x] in R ; :: thesis: x = y
A33: P1[y9,x9] by A5, A32;
P1[x9,y9] by A5, A31;
hence x = y by A2, A33; :: thesis: verum
end;
then R partially_orders F1() by A15, A6;
then consider x being set such that
A34: x is_minimal_in R by A14, A16, Th64;
take x ; :: thesis: ( x is Element of F1() & ( for y being Element of F1() st x <> y holds
not P1[y,x] ) )
thus x is Element of F1() by A14, A34; :: thesis: for y being Element of F1() st x <> y holds
not P1[y,x]
let y be Element of F1(); :: thesis: ( x <> y implies not P1[y,x] )
assume x <> y ; :: thesis: P1[y,x]
then A35: not [y,x] in R by A14, A34;
x in F1() by A14, A34;
hence P1[y,x] by A5, A35; :: thesis: verum