let S1, S2 be strict SubLattStr of L; :: thesis: ( the carrier of S1 = P & the carrier of S2 = P implies S1 = S2 )
assume A1: ( the carrier of S1 = P & the carrier of S2 = P ) ; :: thesis: S1 = S2
A2: the L_join of S1 = the L_join of L || the carrier of S1 by Defx1
.= the L_join of S2 by A1, Defx1 ;
the L_meet of S1 = the L_meet of L || the carrier of S1 by Defx1
.= the L_meet of S2 by A1, Defx1 ;
hence S1 = S2 by A1, A2; :: thesis: verum