let S, T be non empty lower-bounded Poset; :: thesis: ( [:S,T:] is algebraic implies ( S is algebraic & T is algebraic ) )
assume that
A1: for x being Element of [:S,T:] holds
( not compactbelow x is empty & compactbelow x is directed ) and
A2: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_K ) ; :: according to WAYBEL_8:def 4 :: thesis: ( S is algebraic & T is algebraic )
A3: ( S is up-complete & T is up-complete ) by A2, WAYBEL_2:11;

hereby :: according to WAYBEL_8:def 4 :: thesis: T is algebraic

hereby :: thesis: ( S is up-complete & S is satisfying_axiom_K )

let s be Element of S; :: thesis: ( not compactbelow s is empty & compactbelow s is directed )
consider t being Element of T;
A4: [:(compactbelow s),(compactbelow t):] = compactbelow [s,t] by A3, Th50;
A5: proj1 [:(compactbelow s),(compactbelow t):] = compactbelow s by FUNCT_5:11;
compactbelow [s,t] is directed by A1;
hence ( not compactbelow s is empty & compactbelow s is directed ) by A4, A5, YELLOW_3:22; :: thesis: verum

end;

thus S is up-complete by A2, WAYBEL_2:11; :: thesis: S is satisfying_axiom_K
thus S is satisfying_axiom_K :: thesis: verum

proof

let s be Element of S; :: according to WAYBEL_8:def 3 :: thesis: s = "\/" (compactbelow s),S
consider t being Element of T;
( not compactbelow [s,t] is empty & compactbelow [s,t] is directed ) by A1;
then ex_sup_of compactbelow [s,t],[:S,T:] by A2, WAYBEL_0:75;
then A6: sup (compactbelow [s,t]) = [(sup (proj1 (compactbelow [s,t]))),(sup (proj2 (compactbelow [s,t])))] by Th5;
thus s = [s,t] `1 by MCART_1:7
.= (sup (compactbelow [s,t])) `1 by A2, WAYBEL_8:def 3
.= sup (proj1 (compactbelow [s,t])) by A6, MCART_1:7
.= sup (compactbelow ([s,t] `1 )) by A3, Th52
.= sup (compactbelow s) by MCART_1:7 ; :: thesis: verum

end;

end;

hereby :: according to WAYBEL_8:def 4 :: thesis: ( T is up-complete & T is satisfying_axiom_K )

let t be Element of T; :: thesis: ( not compactbelow t is empty & compactbelow t is directed )
consider s being Element of S;
A7: [:(compactbelow s),(compactbelow t):] = compactbelow [s,t] by A3, Th50;
A8: proj2 [:(compactbelow s),(compactbelow t):] = compactbelow t by FUNCT_5:11;
compactbelow [s,t] is directed by A1;
hence ( not compactbelow t is empty & compactbelow t is directed ) by A7, A8, YELLOW_3:22; :: thesis: verum

end;

thus T is up-complete by A2, WAYBEL_2:11; :: thesis: T is satisfying_axiom_K
let t be Element of T; :: according to WAYBEL_8:def 3 :: thesis: t = "\/" (compactbelow t),T
consider s being Element of S;
( not compactbelow [s,t] is empty & compactbelow [s,t] is directed ) by A1;
then ex_sup_of compactbelow [s,t],[:S,T:] by A2, WAYBEL_0:75;
then A9: sup (compactbelow [s,t]) = [(sup (proj1 (compactbelow [s,t]))),(sup (proj2 (compactbelow [s,t])))] by Th5;
thus t = [s,t] `2 by MCART_1:7
.= (sup (compactbelow [s,t])) `2 by A2, WAYBEL_8:def 3
.= sup (proj2 (compactbelow [s,t])) by A9, MCART_1:7
.= sup (compactbelow ([s,t] `2 )) by A3, Th53
.= sup (compactbelow t) by MCART_1:7 ; :: thesis: verum