let S be non empty up-complete Poset; for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)
let T be non empty lower-bounded up-complete Poset; for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)
let x be Element of [:S,T:]; proj1 (waybelow x) = waybelow (x `1)
A1:
Bottom T << x `2
by WAYBEL_3:4;
thus
proj1 (waybelow x) c= waybelow (x `1)
by Th45; XBOOLE_0:def 10 waybelow (x `1) c= proj1 (waybelow x)
let a be object ; TARSKI:def 3 ( not a in waybelow (x `1) or a in proj1 (waybelow x) )
assume A2:
a in waybelow (x `1)
; a in proj1 (waybelow x)
then reconsider a9 = a as Element of S ;
a9 << x `1
by A2, WAYBEL_3:7;
then
[a9,(Bottom T)] << [(x `1),(x `2)]
by A1, Th19;
then A3:
[a9,(Bottom T)] in waybelow [(x `1),(x `2)]
;
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then
x = [(x `1),(x `2)]
by MCART_1:21;
hence
a in proj1 (waybelow x)
by A3, XTUPLE_0:def 12; verum