let S, T be non empty lower-bounded up-complete Poset; :: thesis: ( [:S,T:] is continuous implies ( S is continuous & T is continuous ) )
assume that
A1: for x being Element of [:S,T:] holds
( not waybelow x is empty & waybelow x is directed ) and
A2: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_of_approximation ) ; :: according to WAYBEL_3:def 6 :: thesis: ( S is continuous & T is continuous )
hereby :: according to WAYBEL_3:def 6 :: thesis: T is continuous
hereby :: thesis: ( S is up-complete & S is satisfying_axiom_of_approximation )
set t = the Element of T;
let s be Element of S; :: thesis: ( not waybelow s is empty & waybelow s is directed )
A3: waybelow [s, the Element of T] is directed by A1;
( [:(waybelow s),(waybelow the Element of T):] = waybelow [s, the Element of T] & proj1 [:(waybelow s),(waybelow the Element of T):] = waybelow s ) by Th44, FUNCT_5:9;
hence ( not waybelow s is empty & waybelow s is directed ) by A3, YELLOW_3:22; :: thesis: verum
end;
thus S is up-complete ; :: thesis: S is satisfying_axiom_of_approximation
thus S is satisfying_axiom_of_approximation :: thesis: verum
proof
set t = the Element of T;
let s be Element of S; :: according to WAYBEL_3:def 5 :: thesis: s = "\/" ((waybelow s),S)
waybelow [s, the Element of T] is directed by A1;
then ex_sup_of waybelow [s, the Element of T],[:S,T:] by WAYBEL_0:75;
then A4: sup (waybelow [s, the Element of T]) = [(sup (proj1 (waybelow [s, the Element of T]))),(sup (proj2 (waybelow [s, the Element of T])))] by Th5;
thus s = [s, the Element of T] `1
.= (sup (waybelow [s, the Element of T])) `1 by A2
.= sup (proj1 (waybelow [s, the Element of T])) by A4
.= sup (waybelow ([s, the Element of T] `1)) by Th46
.= sup (waybelow s) ; :: thesis: verum
end;
end;
hereby :: according to WAYBEL_3:def 6 :: thesis: ( T is up-complete & T is satisfying_axiom_of_approximation )
set s = the Element of S;
let t be Element of T; :: thesis: ( not waybelow t is empty & waybelow t is directed )
A5: waybelow [ the Element of S,t] is directed by A1;
( [:(waybelow the Element of S),(waybelow t):] = waybelow [ the Element of S,t] & proj2 [:(waybelow the Element of S),(waybelow t):] = waybelow t ) by Th44, FUNCT_5:9;
hence ( not waybelow t is empty & waybelow t is directed ) by A5, YELLOW_3:22; :: thesis: verum
end;
set s = the Element of S;
thus T is up-complete ; :: thesis: T is satisfying_axiom_of_approximation
let t be Element of T; :: according to WAYBEL_3:def 5 :: thesis: t = "\/" ((waybelow t),T)
now :: thesis: for x being Element of [:S,T:] holds ex_sup_of waybelow x,[:S,T:]
let x be Element of [:S,T:]; :: thesis: ex_sup_of waybelow x,[:S,T:]
( not waybelow x is empty & waybelow x is directed ) by A1;
hence ex_sup_of waybelow x,[:S,T:] by WAYBEL_0:75; :: thesis: verum
end;
then A6: sup (waybelow [ the Element of S,t]) = [(sup (proj1 (waybelow [ the Element of S,t]))),(sup (proj2 (waybelow [ the Element of S,t])))] by Th5;
thus t = [ the Element of S,t] `2
.= (sup (waybelow [ the Element of S,t])) `2 by A2
.= sup (proj2 (waybelow [ the Element of S,t])) by A6
.= sup (waybelow ([ the Element of S,t] `2)) by Th47
.= sup (waybelow t) ; :: thesis: verum