let F be Subset of PL-WFF; :: thesis:
assume Z0: F is consistent ; :: thesis:
set L = PL-WFF ;
consider R being Relation such that
A3: R well_orders PL-WFF by WELLORD2:17;
R /\ [:PL-WFF,PL-WFF:] c= [:PL-WFF,PL-WFF:] by XBOOLE_1:17;
then reconsider R2 = R |_2 PL-WFF as Relation of PL-WFF by WELLORD1:def 6;
R2 well_orders PL-WFF by A3, PCOMPS_2:1;
then A76: R2 is_connected_in PL-WFF by WELLORD1:def 5;
reconsider RS = RelStr(# PL-WFF,R2 #) as non empty RelStr ;
set cRS = the carrier of RS;
defpred S₁[ object , object , object ] means for p being Element of PL-WFF
for f being PartFunc of the carrier of RS,(bool PL-WFF) st $1 = p & $2 = f holds
( ( ((union (rng f)) \/ F) \/ {p} is consistent implies $3 = ((union (rng f)) \/ F) \/ {p} ) & ( not ((union (rng f)) \/ F) \/ {p} is consistent implies $3 = (union (rng f)) \/ F ) );
A4: for x, y being object st x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool PL-WFF)) holds
ex z being object st
( z in bool PL-WFF & S₁[x,y,z] )

proof

let x, y be object ; :: thesis:
assume A6: ( x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool PL-WFF)) ) ; :: thesis:
reconsider x1 = x as Element of PL-WFF by A6;
reconsider y1 = y as PartFunc of the carrier of RS,(bool PL-WFF) by A6, PARTFUN1:46;

per cases ) \/ F) \/ {x1} is consistent or not ((union (rng y1)) \/ F) \/ {x1} is consistent ) ;

suppose A7: ((union (rng y1)) \/ F) \/ {x1} is consistent ; :: thesis:

take ((union (rng y1)) \/ F) \/ {x1} ; :: thesis:
thus ( ((union (rng y1)) \/ F) \/ {x1} in bool PL-WFF & S₁[x,y,((union (rng y1)) \/ F) \/ {x1}] ) by A7; :: thesis:

end;

suppose A7a: not ((union (rng y1)) \/ F) \/ {x1} is consistent ; :: thesis:

take (union (rng y1)) \/ F ; :: thesis:
thus ( (union (rng y1)) \/ F in bool PL-WFF & S₁[x,y,(union (rng y1)) \/ F] ) by A7a; :: thesis:

end;

consider h being Function of [: the carrier of RS,(PFuncs ( the carrier of RS,(bool PL-WFF))):],(bool PL-WFF) such that
A9: for x, y being object st x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool PL-WFF)) holds
S₁[x,y,h . (x,y)] from BINOP_1:sch 1(A4);
R2 well_orders PL-WFF by A3, PCOMPS_2:1;
then R2 is_well_founded_in PL-WFF by WELLORD1:def 5;
then A11: RS is well_founded by WELLFND1:def 2;
then consider f being Function of the carrier of RS,(bool PL-WFF) such that
A12: f is_recursively_expressed_by h by WELLFND1:11;
A73: dom f = the carrier of RS by FUNCT_2:def 1;
reconsider G = union (rng f) as Subset of PL-WFF ;
set iRS = the InternalRel of RS;
F6: field R2 = PL-WFF by A3, PCOMPS_2:1;
A17: for A, B being Element of PL-WFF st [A,B] in R2 holds
f . A c= f . B

proof

let A, B be Element of PL-WFF ; :: thesis:
assume F3: [A,B] in R2 ; :: thesis:

per cases ;

suppose A = B ; :: thesis:

hence f . A c= f . B ; :: thesis:

end;

suppose S2: A <> B ; :: thesis:

F18: now :: thesis:

let x be set ; :: thesis:
assume F19: x in dom (f | ( the InternalRel of RS -Seg A)) ; :: thesis:
thus (f | ( the InternalRel of RS -Seg A)) . x = f . x by F19, FUNCT_1:47
.= (f | ( the InternalRel of RS -Seg B)) . x by F13, FUNCT_1:47, F12, F11, F19 ; :: thesis:

end;

per cases ) \/ F) \/ {A} is consistent or not ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ {A} is consistent ) ;

suppose ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ {A} is consistent ; :: thesis:

per cases ) \/ F) \/ {B} is consistent or not ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} is consistent ) ;

suppose F2a: ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} is consistent ; :: thesis:

F16: f . B = h . (B,(f | ( the InternalRel of RS -Seg B))) by WELLFND1:def 5, A12
.= ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} by A9, E2, F2a ;
thus f . A c= f . B :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in f . A ; :: thesis:
then x in (union (rng (f | ( the InternalRel of RS -Seg B)))) \/ (F \/ {B}) by XBOOLE_0:def 3, F14;
hence x in f . B by F16, XBOOLE_1:4; :: thesis:

end;

suppose F2b: not ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} is consistent ; :: thesis:

F16b: f . B = h . (B,(f | ( the InternalRel of RS -Seg B))) by WELLFND1:def 5, A12
.= (union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F by A9, E2, F2b ;
thus f . A c= f . B by F16b, XBOOLE_0:def 3, F14; :: thesis:

end;

suppose F2: not ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ {A} is consistent ; :: thesis:

F8: f . A = h . (A,(f | ( the InternalRel of RS -Seg A))) by WELLFND1:def 5, A12
.= (union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F by A9, E4, F2 ;

per cases ) \/ F) \/ {B} is consistent or not ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} is consistent ) ;

suppose F2a: ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} is consistent ; :: thesis:

F9: f . B = h . (B,(f | ( the InternalRel of RS -Seg B))) by WELLFND1:def 5, A12
.= ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} by A9, E2, F2a ;
thus f . A c= f . B by F8, F9, XBOOLE_1:10, F7; :: thesis:

end;

suppose F2b: not ((union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F) \/ {B} is consistent ; :: thesis:

f . B = h . (B,(f | ( the InternalRel of RS -Seg B))) by WELLFND1:def 5, A12
.= (union (rng (f | ( the InternalRel of RS -Seg B)))) \/ F by A9, E2, F2b ;
hence f . A c= f . B by F8, XBOOLE_1:9, E1; :: thesis:

end;

A54: rng f is c=-linear

proof

let x be set ; :: according to ORDINAL1:def 8 :: thesis:
let y be set ; :: thesis:
assume B2: ( x in rng f & y in rng f ) ; :: thesis:
then consider x1 being object such that
B3: ( x1 in dom f & f . x1 = x ) by FUNCT_1:def 3;
consider y1 being object such that
B4: ( y1 in dom f & f . y1 = y ) by FUNCT_1:def 3, B2;
reconsider x1 = x1, y1 = y1 as Element of PL-WFF by B3, B4;

per cases ;

suppose x1 = y1 ; :: thesis:

hence x,y are_c=-comparable by B3, B4; :: thesis:

end;

suppose B1: x1 <> y1 ; :: thesis:

per cases in R2 or [y1,x1] in R2 ) by A76, RELAT_2:def 6, B1;

suppose [x1,y1] in R2 ; :: thesis:

then f . x1 c= f . y1 by A17;
hence x,y are_c=-comparable by XBOOLE_0:def 9, B3, B4; :: thesis:

end;

suppose [y1,x1] in R2 ; :: thesis:

then f . y1 c= f . x1 by A17;
hence x,y are_c=-comparable by XBOOLE_0:def 9, B3, B4; :: thesis:

end;

defpred S₂[ Element of RS] means f . $1 is consistent ;

A26: now :: thesis:

let x be Element of RS; :: thesis:
A20: f . x = h . (x,(f | ( the InternalRel of RS -Seg x))) by WELLFND1:def 5, A12;
f | ( the InternalRel of RS -Seg x) in PFuncs ( the carrier of RS,(bool PL-WFF)) by PARTFUN1:45;
hence S₁[x,f | ( the InternalRel of RS -Seg x),f . x] by A20, A9; :: thesis:

end;

A27: now :: thesis:

let x be Element of RS; :: thesis:
reconsider x1 = {x} as Subset of PL-WFF ;
set fr = f | ( the InternalRel of RS -Seg x);

per cases ) \/ F) \/ x1 is consistent or not ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 is consistent ) ;

suppose ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 is consistent ; :: thesis:

then f . x = ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 by A26
.= F \/ ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ x1) by XBOOLE_1:4 ;
hence F c= f . x by XBOOLE_1:7; :: thesis:

end;

suppose not ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 is consistent ; :: thesis:

then f . x = F \/ (union (rng (f | ( the InternalRel of RS -Seg x)))) by A26;
hence F c= f . x by XBOOLE_1:7; :: thesis:

end;

A21: for x being Element of RS st ( for y being Element of RS st y <> x & [y,x] in the InternalRel of RS holds
S₂[y] ) holds
S₂[x]

proof

per cases ) \/ F) \/ x1 is consistent or not ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 is consistent ) ;

suppose ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 is consistent ; :: thesis:

hence S₂[x] by A26; :: thesis:

end;

suppose C1: not ((union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F) \/ x1 is consistent ; :: thesis:

then A22: f . x = (union (rng (f | ( the InternalRel of RS -Seg x)))) \/ F by A26;

per cases ;

suppose S4: for y being object holds
( not [y,x] in the InternalRel of RS or y = x ) ; :: thesis:

the InternalRel of RS -Seg x = {}

proof

assume the InternalRel of RS -Seg x <> {} ; :: thesis:
then consider y being object such that
F19: y in the InternalRel of RS -Seg x by XBOOLE_0:7;
( y <> x & [y,x] in the InternalRel of RS ) by WELLORD1:1, F19;
hence contradiction by S4; :: thesis:

end;

then dom (f | ( the InternalRel of RS -Seg x)) = {} by FUNCT_2:def 1, C2;
then rng (f | ( the InternalRel of RS -Seg x)) = {} by RELAT_1:42;
hence S₂[x] by Z0, ZFMISC_1:2, A26, C1; :: thesis:

end;

suppose A39: ex y being object st
( [y,x] in the InternalRel of RS & y <> x ) ; :: thesis:

end;

A13a: for A being Element of RS holds S₂[A] from WELLFND1:sch 3(A21, A11);
take G ; :: thesis:
thus F c= G :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A46: y in F ; :: thesis:
set z = the Element of RS;
A47: F c= f . the Element of RS by A27;
f . the Element of RS in rng f by FUNCT_1:3, A73;
hence y in G by A46, A47, TARSKI:def 4; :: thesis:

end;

thus G is consistent :: thesis:

proof

assume not G is consistent ; :: thesis:
then consider F being Subset of PL-WFF such that
A14: ( F is finite & not F is consistent & F c= G ) by finin;
consider z being set such that
A90: ( F c= z & z in rng f ) by uniolinf, A14, A54, RELAT_1:42, A73;
rng f c= bool PL-WFF ;
then reconsider z = z as Subset of PL-WFF by A90;
consider x being object such that
A92: ( x in dom f & f . x = z ) by A90, FUNCT_1:def 3;
thus contradiction by A92, A13a, A90, A14, incsub; :: thesis:

end;

thus G is maximal :: thesis:

proof

given A being Element of PL-WFF such that A71: ( not A in G & not 'not' A in G ) ; :: according to PL_AXIOM:def 28 :: thesis:
reconsider ARS = A as Element of RS ;
reconsider nA = 'not' A as Element of RS ;
set fA = f | ( the InternalRel of RS -Seg A);
set fnA = f | ( the InternalRel of RS -Seg ('not' A));
reconsider A1 = {A} as Subset of PL-WFF ;
reconsider A1n = {('not' A)} as Subset of PL-WFF ;
A74: not ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ A1 is consistent

proof

assume ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ A1 is consistent ; :: thesis:
then A70: f . ARS = ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ A1 by A26;
ARS in A1 by TARSKI:def 1;
then C1: ARS in ((union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F) \/ A1 by XBOOLE_0:def 3;
f . ARS in rng f by FUNCT_1:3, A73;
hence contradiction by TARSKI:def 4, A71, A70, C1; :: thesis:

end;

A78: not ((union (rng (f | ( the InternalRel of RS -Seg ('not' A))))) \/ F) \/ A1n is consistent

proof

assume ((union (rng (f | ( the InternalRel of RS -Seg ('not' A))))) \/ F) \/ A1n is consistent ; :: thesis:
then A70a: f . nA = ((union (rng (f | ( the InternalRel of RS -Seg ('not' A))))) \/ F) \/ A1n by A26;
nA in A1n by TARSKI:def 1;
then A72a: nA in f . nA by A70a, XBOOLE_0:def 3;
f . nA in rng f by FUNCT_1:3, A73;
hence contradiction by TARSKI:def 4, A71, A72a; :: thesis:

end;

then A80: f . nA = (union (rng (f | ( the InternalRel of RS -Seg ('not' A))))) \/ F by A26;
A79: f . A = (union (rng (f | ( the InternalRel of RS -Seg A)))) \/ F by A26, A74;
reconsider AAA = A as Element of HP-WFF by plhp;
reconsider fal = FaLSUM as Element of HP-WFF by plhp;
AAA => fal = A => FaLSUM ;
then len A <> len ('not' A) by HILBERT2:16;

per cases in R2 or [('not' A),A] in R2 ) by A76, RELAT_2:def 6;

suppose [A,('not' A)] in R2 ; :: thesis:

then f . A c= f . nA by A17;
then not (f . nA) \/ A1 is consistent by A74, incsub, A79, XBOOLE_1:9;
hence contradiction by A13a, onecon, A78, A80; :: thesis:

end;

suppose [('not' A),A] in R2 ; :: thesis:

then f . nA c= f . A by A17;
then not (f . ARS) \/ A1n is consistent by A78, incsub, A80, XBOOLE_1:9;
hence contradiction by onecon, A74, A79, A13a; :: thesis:

end;