let BL be non trivial B_Lattice; :: thesis: for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)

let a, b be Element of BL; :: thesis: (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)

A1: (UFilter BL) . (a "\/" b) c= ((UFilter BL) . a) \/ ((UFilter BL) . b)

let a, b be Element of BL; :: thesis: (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)

A1: (UFilter BL) . (a "\/" b) c= ((UFilter BL) . a) \/ ((UFilter BL) . b)

proof

((UFilter BL) . a) \/ ((UFilter BL) . b) c= (UFilter BL) . (a "\/" b)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UFilter BL) . (a "\/" b) or x in ((UFilter BL) . a) \/ ((UFilter BL) . b) )

set c = a "\/" b;

assume x in (UFilter BL) . (a "\/" b) ; :: thesis: x in ((UFilter BL) . a) \/ ((UFilter BL) . b)

then consider F0 being Filter of BL such that

A2: x = F0 and

A3: F0 is being_ultrafilter and

A4: a "\/" b in F0 by Th17;

( a in F0 or b in F0 ) by A3, A4, Th19;

then ( F0 in (UFilter BL) . a or F0 in (UFilter BL) . b ) by A3, Th17;

hence x in ((UFilter BL) . a) \/ ((UFilter BL) . b) by A2, XBOOLE_0:def 3; :: thesis: verum

end;set c = a "\/" b;

assume x in (UFilter BL) . (a "\/" b) ; :: thesis: x in ((UFilter BL) . a) \/ ((UFilter BL) . b)

then consider F0 being Filter of BL such that

A2: x = F0 and

A3: F0 is being_ultrafilter and

A4: a "\/" b in F0 by Th17;

( a in F0 or b in F0 ) by A3, A4, Th19;

then ( F0 in (UFilter BL) . a or F0 in (UFilter BL) . b ) by A3, Th17;

hence x in ((UFilter BL) . a) \/ ((UFilter BL) . b) by A2, XBOOLE_0:def 3; :: thesis: verum

proof

hence
(UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((UFilter BL) . a) \/ ((UFilter BL) . b) or x in (UFilter BL) . (a "\/" b) )

assume x in ((UFilter BL) . a) \/ ((UFilter BL) . b) ; :: thesis: x in (UFilter BL) . (a "\/" b)

then ( x in (UFilter BL) . a or x in (UFilter BL) . b ) by XBOOLE_0:def 3;

then ( ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & a in F0 ) or ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & b in F0 ) ) by Th17;

then consider F0 being Filter of BL such that

A5: x = F0 and

A6: F0 is being_ultrafilter and

A7: ( a in F0 or b in F0 ) ;

a "\/" b in F0 by A6, A7, Th19;

hence x in (UFilter BL) . (a "\/" b) by A5, A6, Th17; :: thesis: verum

end;assume x in ((UFilter BL) . a) \/ ((UFilter BL) . b) ; :: thesis: x in (UFilter BL) . (a "\/" b)

then ( x in (UFilter BL) . a or x in (UFilter BL) . b ) by XBOOLE_0:def 3;

then ( ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & a in F0 ) or ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & b in F0 ) ) by Th17;

then consider F0 being Filter of BL such that

A5: x = F0 and

A6: F0 is being_ultrafilter and

A7: ( a in F0 or b in F0 ) ;

a "\/" b in F0 by A6, A7, Th19;

hence x in (UFilter BL) . (a "\/" b) by A5, A6, Th17; :: thesis: verum