{ a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) } c= the carrier of L

( not a = b "\/" c or a = b or a = c ) ) ) } is Subset of L ; :: thesis: verum

( not a = b "\/" c or a = b or a = c ) ) ) } c= the carrier of L

proof

hence
{ a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) } or x in the carrier of L )

assume x in { a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) } ; :: thesis: x in the carrier of L

then ex a being Element of L st

( x = a & a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) ;

hence x in the carrier of L ; :: thesis: verum

end;( not a = b "\/" c or a = b or a = c ) ) ) } or x in the carrier of L )

assume x in { a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) } ; :: thesis: x in the carrier of L

then ex a being Element of L st

( x = a & a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) ;

hence x in the carrier of L ; :: thesis: verum

( not a = b "\/" c or a = b or a = c ) ) ) } is Subset of L ; :: thesis: verum