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 )
set t = the Element of T;
let s be Element of S; :: thesis: ( not compactbelow s is empty & compactbelow s is directed )
A4: compactbelow [s, the Element of T] is directed by A1;
( [:(compactbelow s),(compactbelow the Element of T):] = compactbelow [s, the Element of T] & proj1 [:(compactbelow s),(compactbelow the Element of T):] = compactbelow s ) by A3, Th50, FUNCT_5:9;
hence ( not compactbelow s is empty & compactbelow s is directed ) by A4, 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
set t = the Element of T;
let s be Element of S; :: according to WAYBEL_8:def 3 :: thesis: s = "\/" ((compactbelow s),S)
( not compactbelow [s, the Element of T] is empty & compactbelow [s, the Element of T] is directed ) by A1;
then ex_sup_of compactbelow [s, the Element of T],[:S,T:] by A2, WAYBEL_0:75;
then A5: sup (compactbelow [s, the Element of T]) = [(sup (proj1 (compactbelow [s, the Element of T]))),(sup (proj2 (compactbelow [s, the Element of T])))] by Th5;
thus s = [s, the Element of T] `1
.= (sup (compactbelow [s, the Element of T])) `1 by A2
.= sup (proj1 (compactbelow [s, the Element of T])) by A5
.= sup (compactbelow ([s, the Element of T] `1)) by A3, Th52
.= sup (compactbelow s) ; :: thesis: verum
end;
end;
set s = the Element of S;
hereby :: according to WAYBEL_8:def 4 :: thesis: ( T is up-complete & T is satisfying_axiom_K )
set s = the Element of S;
let t be Element of T; :: thesis: ( not compactbelow t is empty & compactbelow t is directed )
A6: compactbelow [ the Element of S,t] is directed by A1;
( [:(compactbelow the Element of S),(compactbelow t):] = compactbelow [ the Element of S,t] & proj2 [:(compactbelow the Element of S),(compactbelow t):] = compactbelow t ) by A3, Th50, FUNCT_5:9;
hence ( not compactbelow t is empty & compactbelow t is directed ) by A6, 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)
( not compactbelow [ the Element of S,t] is empty & compactbelow [ the Element of S,t] is directed ) by A1;
then ex_sup_of compactbelow [ the Element of S,t],[:S,T:] by A2, WAYBEL_0:75;
then A7: sup (compactbelow [ the Element of S,t]) = [(sup (proj1 (compactbelow [ the Element of S,t]))),(sup (proj2 (compactbelow [ the Element of S,t])))] by Th5;
thus t = [ the Element of S,t] `2
.= (sup (compactbelow [ the Element of S,t])) `2 by A2
.= sup (proj2 (compactbelow [ the Element of S,t])) by A7
.= sup (compactbelow ([ the Element of S,t] `2)) by A3, Th53
.= sup (compactbelow t) ; :: thesis: verum