A1: not { (uparrow i) where i is Element of L : verum } is empty

proof

set l0 = the Element of L;
take uparrow the Element of L ; :: according to XBOOLE_0:def 1 :: thesis: uparrow the Element of L in { (uparrow i) where i is Element of L : verum }
thus uparrow the Element of L in { (uparrow i) where i is Element of L : verum } ; :: thesis: verum

end;

{ (uparrow i) where i is Element of L : verum } c= bool the carrier of L

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (uparrow i) where i is Element of L : verum } or t in bool the carrier of L )
assume t in { (uparrow i) where i is Element of L : verum } ; :: thesis: t in bool the carrier of L
then consider i0 being Element of L such that
A2: t = uparrow i0 ;
thus t in bool the carrier of L by A2; :: thesis: verum

end;

hence { (uparrow i) where i is Element of L : verum } is non empty Subset-Family of L by A1; :: thesis: verum