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 )

A3: now

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;

hereby :: according to WAYBEL_3:def 6 :: thesis: T is continuous

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

let s be Element of S; :: thesis: ( not waybelow s is empty & waybelow s is directed )
consider t being Element of T;
A4: [:(waybelow s),(waybelow t):] = waybelow [s,t] by Th44;
A5: proj1 [:(waybelow s),(waybelow t):] = waybelow s by FUNCT_5:11;
waybelow [s,t] is directed by A1;
hence ( not waybelow s is empty & waybelow s is directed ) by A4, A5, 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

let s be Element of S; :: according to WAYBEL_3:def 5 :: thesis: s = "\/" (waybelow s),S
consider t being Element of T;
waybelow [s,t] is directed by A1;
then ex_sup_of waybelow [s,t],[:S,T:] by WAYBEL_0:75;
then A6: sup (waybelow [s,t]) = [(sup (proj1 (waybelow [s,t]))),(sup (proj2 (waybelow [s,t])))] by Th5;
thus s = [s,t] `1 by MCART_1:7
.= (sup (waybelow [s,t])) `1 by A2, WAYBEL_3:def 5
.= sup (proj1 (waybelow [s,t])) by A6, MCART_1:7
.= sup (waybelow ([s,t] `1 )) by Th46
.= sup (waybelow s) by MCART_1:7 ; :: thesis: verum

end;

end;

hereby :: according to WAYBEL_3:def 6 :: thesis: ( T is up-complete & T is satisfying_axiom_of_approximation )

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

end;

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
consider s being Element of S;
ex_sup_of waybelow [s,t],[:S,T:] by A3;
then A9: sup (waybelow [s,t]) = [(sup (proj1 (waybelow [s,t]))),(sup (proj2 (waybelow [s,t])))] by Th5;
thus t = [s,t] `2 by MCART_1:7
.= (sup (waybelow [s,t])) `2 by A2, WAYBEL_3:def 5
.= sup (proj2 (waybelow [s,t])) by A9, MCART_1:7
.= sup (waybelow ([s,t] `2 )) by Th47
.= sup (waybelow t) by MCART_1:7 ; :: thesis: verum