let X, Y be LeftIdeal of L; :: thesis: ( F c= X & ( for I being LeftIdeal of L st F c= I holds
X c= I ) & F c= Y & ( for I being LeftIdeal of L st F c= I holds
Y c= I ) implies X = Y )
assume ( F c= X & ( for I being LeftIdeal of L st F c= I holds
X c= I ) & F c= Y & ( for I being LeftIdeal of L st F c= I holds
Y c= I ) ) ; :: thesis: X = Y
then ( X c= Y & Y c= X ) ;
hence X = Y by XBOOLE_0:def 10; :: thesis: verum