let S be non empty up-complete Poset; :: thesis: for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1 )
let T be non empty lower-bounded up-complete Poset; :: thesis: for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1 )
let x be Element of [:S,T:]; :: thesis: proj1 (compactbelow x) = compactbelow (x `1 )
A1: Bottom T <= x `2 by YELLOW_0:44;
thus proj1 (compactbelow x) c= compactbelow (x `1 ) by Th51; :: according to XBOOLE_0:def 10 :: thesis: compactbelow (x `1 ) c= proj1 (compactbelow x)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in compactbelow (x `1 ) or a in proj1 (compactbelow x) )
assume A2: a in compactbelow (x `1 ) ; :: thesis: a in proj1 (compactbelow x)
then reconsider a9 = a as Element of S ;
a9 <= x `1 by A2, WAYBEL_8:4;
then A3: [a9,(Bottom T)] <= [(x `1 ),(x `2 )] by A1, YELLOW_3:11;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then A4: x = [(x `1 ),(x `2 )] by MCART_1:23;
A5: ( [a9,(Bottom T)] `1 = a9 & [a9,(Bottom T)] `2 = Bottom T ) by MCART_1:7;
a9 is compact by A2, WAYBEL_8:4;
then [a9,(Bottom T)] is compact by A5, Th23, WAYBEL_3:15;
then [a9,(Bottom T)] in compactbelow [(x `1 ),(x `2 )] by A3;
hence a in proj1 (compactbelow x) by A4, RELAT_1:def 4; :: thesis: verum