let S, T be non empty up-complete Poset; 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; for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]
let t be Element of T; [:(wayabove s),(wayabove t):] = wayabove [s,t]
hereby TARSKI:def 3,
XBOOLE_0:def 10 wayabove [s,t] c= [:(wayabove s),(wayabove t):]
let x be
object ;
( x in [:(wayabove s),(wayabove t):] implies x in wayabove [s,t] )assume
x in [:(wayabove s),(wayabove t):]
;
x in wayabove [s,t]then consider x1,
x2 being
object 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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in wayabove [s,t] or x in [:(wayabove s),(wayabove t):] )
assume A4:
x in wayabove [s,t]
; x in [:(wayabove s),(wayabove t):]
then reconsider x9 = 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:
x9 = [(x9 `1),(x9 `2)]
by MCART_1:21;
A6:
[s,t] << x9
by A4, WAYBEL_3:8;
then
t << x9 `2
by A5, Th19;
then A7:
x `2 in wayabove t
;
s << x9 `1
by A5, A6, Th19;
then
x `1 in wayabove s
;
hence
x in [:(wayabove s),(wayabove t):]
by A5, A7, ZFMISC_1:def 2; verum