let X be non empty set ; :: thesis: for B being non empty Subset of (BoolePoset X) holds
( ( for x, y being Element of B ex z being Element of B st z c= x /\ y ) iff B is filtered )
let B be non empty Subset of (BoolePoset X); :: thesis: ( ( for x, y being Element of B ex z being Element of B st z c= x /\ y ) iff B is filtered )

hereby :: thesis: ( B is filtered implies for x, y being Element of B ex z being Element of B st z c= x /\ y )

assume A1: for x, y being Element of B ex z being Element of B st z c= x /\ y ; :: thesis: B is filtered
for x, y being Element of (BoolePoset X) st x in B & y in B holds
ex z being Element of (BoolePoset X) st
( z in B & z <= x & z <= y )

proof

let x, y be Element of (BoolePoset X); :: thesis: ( x in B & y in B implies ex z being Element of (BoolePoset X) st
( z in B & z <= x & z <= y ) )
assume A2: ( x in B & y in B ) ; :: thesis: ex z being Element of (BoolePoset X) st
( z in B & z <= x & z <= y )
reconsider x = x, y = y as Element of B by A2;
consider z0 being Element of B such that
A3: z0 c= x /\ y by A1;
reconsider z0 = z0 as Element of (BoolePoset X) ;
take z0 ; :: thesis: ( z0 in B & z0 <= x & z0 <= y )
( x /\ y c= x & x /\ y c= y ) by XBOOLE_1:17;
then ( z0 c= x & z0 c= y ) by A3;
hence ( z0 in B & z0 <= x & z0 <= y ) by YELLOW_1:2; :: thesis: verum

end;

hence B is filtered ; :: thesis: verum

end;

assume A4: B is filtered ; :: thesis: for x, y being Element of B ex z being Element of B st z c= x /\ y
for x, y being Element of B ex z being Element of B st z c= x /\ y

proof

let x, y be Element of B; :: thesis: ex z being Element of B st z c= x /\ y
consider z0 being Element of (BoolePoset X) such that
A5: z0 in B and
A6: z0 <= x and
A7: z0 <= y by A4;
A8: ( z0 c= x & z0 c= y ) by A6, A7, YELLOW_1:2;
reconsider z0 = z0 as Element of B by A5;
take z0 ; :: thesis: z0 c= x /\ y
thus z0 c= x /\ y by A8, XBOOLE_1:19; :: thesis: verum

end;

hence for x, y being Element of B ex z being Element of B st z c= x /\ y ; :: thesis: verum