let S, T be non empty up-complete Poset; :: thesis: for s being Element of S
for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]
let s be Element of S; :: thesis: for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]
let t be Element of T; :: thesis: [:(wayabove s),(wayabove t):] = wayabove [s,t]

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: wayabove [s,t] c= [:(wayabove s),(wayabove t):]

let x be set ; :: thesis: ( x in [:(wayabove s),(wayabove t):] implies x in wayabove [s,t] )
assume x in [:(wayabove s),(wayabove t):] ; :: thesis: x in wayabove [s,t]
then consider x1, x2 being set such that
A1: x1 in wayabove s and
A2: x2 in wayabove t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
( s << x1 & t << x2 ) by A1, A2, WAYBEL_3:8;
then [s,t] << [x1,x2] by Th19;
hence x in wayabove [s,t] by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in wayabove [s,t] or x in [:(wayabove s),(wayabove t):] )
assume A4: x in wayabove [s,t] ; :: thesis: x in [:(wayabove s),(wayabove t):]
then reconsider x' = x as Element of [:S,T:] ;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then A5: x' = [(x' `1 ),(x' `2 )] by MCART_1:23;
A6: [s,t] << x' by A4, WAYBEL_3:8;
then t << x' `2 by A5, Th19;
then A7: x `2 in wayabove t ;
s << x' `1 by A5, A6, Th19;
then x `1 in wayabove s ;
hence x in [:(wayabove s),(wayabove t):] by A5, A7, MCART_1:11; :: thesis: verum