let S be non empty lower-bounded up-complete Poset; :: thesis: for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2 )
let T be non empty up-complete Poset; :: thesis: for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2 )
let x be Element of [:S,T:]; :: thesis: proj2 (waybelow x) = waybelow (x `2 )
A1: Bottom S << x `1 by WAYBEL_3:4;
thus proj2 (waybelow x) c= waybelow (x `2 ) by Th45; :: according to XBOOLE_0:def 10 :: thesis: waybelow (x `2 ) c= proj2 (waybelow x)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in waybelow (x `2 ) or a in proj2 (waybelow x) )
assume A2: a in waybelow (x `2 ) ; :: thesis: a in proj2 (waybelow x)
then reconsider a9 = a as Element of T ;
a9 << x `2 by A2, WAYBEL_3:7;
then [(Bottom S),a9] << [(x `1 ),(x `2 )] by A1, Th19;
then A3: [(Bottom S),a9] 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:23;
hence a in proj2 (waybelow x) by A3, RELAT_1:def 5; :: thesis: verum